1) XXX[J,RED] and 2) SUM[J,RED]	8-07-79 07:53	pages 1,1

**** File 1) XXX[J,RED], Page 1 line 1
1)	COMMENT ⊗   VALID 00008 PAGES
1)	C REC  PAGE   DESCRIPTION
**** File 2) SUM[J,RED], Page 1 line 1
2)	COMMENT ⊗   VALID 00009 PAGES
2)	C REC  PAGE   DESCRIPTION
***************


**** File 1) XXX[J,RED], Page 1 line 5
1)	C00014 00003	.cent(Specification Language)
1)	C00021 00004	.P2:
1)	C00023 00005	.cent(Intermediate Language)
1)	C00027 00006	.cent(Correctness of the Mapping to Intermediate Form)
1)	C00033 00007	.cent(Conclusions and Further Research)
1)	C00043 00008	.bib
1)	C00055 ENDMK
1)	C⊗;
**** File 2) SUM[J,RED], Page 1 line 5
2)	C00018 00003	.cent(Specification Language)
2)	C00029 00004	.P2:
2)	C00039 00005	.cent(Intermediate Language)
2)	C00052 00006	.cent(Correctness of the Mapping to Intermediate Form)
2)	C00058 00007	.cent(Mapping the Intermediate Language to LISP)
2)	C00063 00008	.cent(Conclusions and Further Research)
2)	C00073 00009	.bib
2)	C00089 ENDMK
2)	C⊗;
***************


**** File 1) XXX[J,RED], Page 7 line 1
1)	.cent(Conclusions and Further Research)
**** File 2) SUM[J,RED], Page 7 line 1
2)	.cent(Mapping the Intermediate Language to LISP)
2)	We have chosen to use LISP as the first target language.  
2)	We generate
2)	"pure LISP" programs.
2)	The function %dL%1, mapping the intermediate language into LISP is defined
2)	in the thesis.
2)	There is no mapping of generic definitions, only of the specific function definitions
2)	involved. We define a
2)	LISP function %3bktrkcond%1 that evaluates its arguments, binds the results
2)	to the formal parameters %3actuals%1 and %3list-alts%1, and then 
2)	recursively attempts each
2)	alternative until an answer is found or all alternatives have failed, indicating
2)	that the answer is undefined.
2)	The LISP program that is generated from the specification for the factorial
  1) XXX[J,RED] and 2) SUM[J,RED]	8-07-79 07:53	pages 7,7

2)	function is as follows. The auxiliary information is put on the property list
2)	of the function name so it is accessible when needed.  The
2)	actual LISP definition of the function is accomplished with a %3defun%1.
2)	.begin nofill;select 3
2)	.group
2)	(defun Fact fexpr (l) 
2)	       (cond ((true-precond (cons 'Fact l))
2)		      (bktrkcond l
2)				 '(((0 1) (try))
2)				   ((!x !y)
2)				    (try (Sub1 !x !x1)
2)					 (Fact !x1 !y1)
2)					 (* !x !y1 !y))))))
2)		     (t 'undef)))
2)	.apart
2)	.end
2)	In the thesis we prove that the semantics of the LISP form of a function or
2)	type definition is equivalent to the semantics of the intermediate form.
2)	.cent(Conclusions and Further Research)
***************